﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using SimpleIR;
using System.Diagnostics.Contracts;

namespace RgnAnalyzer.Domain
{
	/// <summary>
	/// Support for simple numeric tracking of if a value is 0, 1, or unknown.
	/// </summary>
	internal static class ZeroOne
	{
		internal enum Value : byte
		{
			Zero,
			One,
			Unknown
		};

		public static Value IntToValue(long i)
		{
			if(i == 0)
				return Value.Zero;
			else if(i == 1)
				return Value.One;
			else
				return Value.Unknown;
		}

		public static Value IntToValue(ulong i)
		{
			if(i == 0)
				return Value.Zero;
			else if(i == 1)
				return Value.One;
			else
				return Value.Unknown;
		}

		/// <summary>
		/// Return the join of the two zero/one values
		/// </summary>
		public static Value JoinValues(Value v1, Value v2)
		{
			if(v1 == v2)
				return v1;
			else
				return Value.Unknown;
		}

		/// <summary>
		/// Return true if the two zero/one values are equivalent in the abstract domain sense.
		/// </summary>
		public static bool EquivValues(Value v1, Value v2)
		{ return (v1 == v2); }

		/// <summary>
		/// Return the result for if the two zero/one values must be equal during concrete program execution.
		/// </summary>
		public static Value Equal_Simulate(Value v1, Value v2)
		{
			if(v1 == Value.Zero)
			{
				if(v2 == Value.Zero)
					return Value.One;
				else if(v2 == Value.One)
					return Value.Zero;
				else
					return Value.Unknown;
			}
			else if(v1 == Value.One)
			{
				if(v2 == Value.One)
					return Value.One;
				else if(v2 == Value.Zero)
					return Value.Zero;
				else
					return Value.Unknown;
			}
			else
				return Value.Unknown;
		}

		/// <summary>
		/// Return the result for if the two zero/one values must be v1 lessthan v2 during concrete program execution.
		/// </summary>
		public static Value Less_Simulate(Value v1, Value v2)
		{
			if(v1 == Value.Zero)
			{
				if(v2 == Value.Zero)
					return Value.Zero;
				else if(v2 == Value.One)
					return Value.One;
				else
					return Value.Unknown;
			}
			else if(v1 == Value.One)
			{
				if(v2 == Value.One)
					return Value.Zero;
				else if(v2 == Value.Zero)
					return Value.Zero;
				else
					return Value.Unknown;
			}
			else
				return Value.Unknown;
		}

		/// <summary>
		/// Return the value One if the input Zero, Zero if the input is One and Unknown otherwise.
		/// </summary>
		public static Value LogicalNot_Simulate(Value v)
		{
			if(v == Value.One)
				return Value.Zero;
			else if(v == Value.Zero)
				return Value.One;
			else
				return Value.Unknown;
		}

		/// <summary>
		/// Return the value One if one of the two zero/one values are One, Zero if they are both Zero and Unknown otherwise.
		/// </summary>
		public static Value LogicalOr_Simulate(Value v1, Value v2)
		{
			if((v1 == Value.One) | (v2 == Value.One))
				return Value.One;
			else if((v1 == Value.Zero) & (v2 == Value.Zero))
				return Value.Zero;
			else
				return Value.Unknown;
		}

		/// <summary>
		/// Return the value One if both of the two zero/one values are One, Zero if either are both Zero and Unknown otherwise.
		/// </summary>
		public static Value LogicalAnd_Simulate(Value v1, Value v2)
		{
			if((v1 == Value.One) & (v2 == Value.One))
				return Value.One;
			else if((v1 == Value.Zero) | (v2 == Value.Zero))
				return Value.Zero;
			else
				return Value.Unknown;
		}

		/// <summary>
		/// Convert the value information into a nice string.
		/// </summary>
		internal static string ConvertValueToString(Value vv)
		{
			switch(vv)
			{
				case Value.Zero:
					return "0";
				case Value.One:
					return "1";
				case Value.Unknown:
					return "U";
				default:
					Contract.Assert(false, "BAD CASE");
					return "ERROR";
			}
		}
	}
}
